functor VcGen (S : VCGEN_STRUCTS) : VCGEN =
struct
  open S
  
  structure I = Ir
  structure T = Temp
  structure Types = Ir.Types
  structure Set = Set.StringBSet
  structure V = Irvc2vc
  
  local open I
  in structure Id = Id
     structure Intl = Intl
  end
  
  val e_set = Set.empty
  val funcs = ref [(Id.fromString "",[(Id.fromString "",I.Void)],I.Expvoid,I.Expvoid)]
  
  val vopt = ref true
  fun open_vopt() = (vopt:=true)
  fun close_vopt() = (vopt:=false)
 
  val l_vclist : (Id.t * I.exp) list ref = ref []

  fun new_lvc prop1 prop2 pos = 
      let val lvcname = "_L"^(T.gen_name pos)
      in  l_vclist := (Id.fromString (lvcname^"_ne"), prop2) :: (Id.fromString (lvcname^"_e"), prop1) :: (!l_vclist)
      end

  fun get_lvc () = List.rev (!l_vclist)
  fun reset_lvc () = (l_vclist := [])

  fun conj (p1, p2, pos) =
      case (p1, p2)
       of (I.Expvoid, p2) => p2
        | (p1, I.Expvoid) => p1
        | (p1, p2) => 
          if (!vopt)
          then let fun break (I.BinopExp(e1, I.Band, e2, pos)) = (break e1) @ (break e2)
                     | break x = [x]
                   val new_p1 = break p1
                   val new_p2 = V.tr_e p2
                   fun check e = ((V.tr_e e) = new_p2)
                   fun new_p1'() =
                       if (List.exists check new_p1)
                       then p1
                       else I.BinopExp(p1, I.Band, p2, pos)
               in  new_p1'()
               end
          else I.BinopExp(p1, I.Band, p2, pos)
  
  fun split (I.Seq(I.Prop(prop, pos), stmt, pos1)) = (prop, stmt)
    | split (_) = raise Fail "why not a prop here...\n"
  
  fun side_exp e =
      case e
       of I.Expvoid => I.Expvoid
        | I.IntNum(i) => I.Expvoid
        | I.True => I.Expvoid
        | I.False => I.Expvoid
        | I.Null => I.Expvoid
        | I.Lval(l) => side_lval l
        | I.BinopExp(e1, bop, e2, pos) => 
          let val (prop1, prop2) = (side_exp e1, side_exp e2)
          in  conj(prop1, prop2, pos)
          end 
        | I.Not(e, p) => side_exp e
        | I.Result => I.Expvoid
        | I.Imply(e1, e2, pos) => conj(side_exp e1, side_exp e2, pos)
        | I.Forall(id, ty, e, pos) => side_exp e
        | I.Exists(id, ty, e, pos) => side_exp e
        | I.Pi(_, _) => raise Fail "not implemented\n"
        | I.N(_, _) => raise Fail "not implemented\n"
        | I.D(_, _) => raise Fail "not implemented\n"
        | I.Prev(_, _) => raise Fail "not implemented\n"
        | I.LList(exp, pos) => side_exp exp
        | I.Tree(exp, pos) => side_exp exp
        | _ => raise Fail ""

  and side_lval lval =
      case lval
       of I.Var(id, p) => I.Expvoid
        | I.Ptr(sharp_node, lv0, pos) =>
          let val sel_node = I.selectL lv0
              val prop = side_lval lv0
          in  conj (I.BinopExp(I.Lval(sel_node), I.NEqu, I.Null, pos), prop, pos)
          end
        | I.Inarray(lv0, e, size, pos) => 
          let val tmpprop1 = side_lval lv0
              val tmpprop2 = side_exp e
              val tmpprop = conj(tmpprop1, tmpprop2, pos)
              val sel_e = I.selectE e
              val prop1 = I.BinopExp(sel_e, I.GE, I.IntNum(0), pos)
              val prop2 = I.BinopExp(sel_e, I.LT, I.IntNum(size), pos)
              val tmpprop' = conj (prop1, prop2, pos)
          in  conj(tmpprop, tmpprop', pos)
          end
        | I.Instruct(lv0,id0,pos) => side_lval lv0
        | I.Instruct2 (lv0, id0, id, pos) => side_lval lv0
        | _ => raise Fail "no this case, compiler error\n"
                                
  fun side_es ([], pos) = I.Expvoid
    | side_es (x::xs, pos) = conj(side_es (xs, pos), side_exp x, pos)

  fun f_alist(id, pos) = 
      let fun argname([]) = []
	    | argname((a0,t0)::l) = 
	      I.Var(a0,pos)::argname(l)
	  fun find([]) = []
	    | find((fid,alist,prec,postc)::l) = 
	      if Id.equals (fid, id)
	      then alist
	      else find(l)
	  val args = find(!funcs)
      in argname(args)
      end

  fun f_pre_post id = 
      let fun find([]) = raise Fail "why not this function"
	    | find((fid, alist, pre, post)::xs) = 
	      if Id.equals (fid, id)
	      then (pre, post)
	      else find xs
      in  find (!funcs)
      end

  fun vcgensimple(var, upd) = 
      let fun eq(I.Var(id0, _), I.Var(id1, _)) = 
	      if Id.equals (id0, id1)
	      then true
	      else false 
	    | eq _ = false
	  fun repvar(I.Var(id0, p0), I.Var(id1, p1)) = I.Var(id1, p0)
	    | repvar(ivar0, ivar1) = ivar1
	  fun simplify(updnode) = 
	      case updnode
	       of (I.Upd(var1,I.Expvoid,I.Lval(lval2))) => 
		  repvar(var1,lval2)
		| (I.Upd(var1,exp1,exp2)) => (I.Upd(var1,exp1,exp2))
		| _ => (print("error in vcgensimple"); updnode)
	  fun map (I.Upd(var1, exp1, exp2)) = 
	      if(eq(var, var1))
	      then simplify upd
	      else var
	    | map _ = var
      in  map upd
      end 

  fun subst_exp (exp, subexp, newsub) =
      case exp
       of I.Expvoid => I.Expvoid
	| I.IntNum(i) => I.IntNum(i)
	| I.True => I.True
	| I.False => I.False
	| I.Null => I.Null
	| I.Lval(l) => 
	  let val tmpres = subst_lval(l, subexp, newsub)
	  in  case tmpres
	       of (I.Upd(lv1, I.Expvoid, e0)) => e0
		| _ => I.Lval(tmpres)
	  end
	| I.BinopExp(e1, bop, e2, pos) => 
	  let val nexp1 = subst_exp (e1, subexp, newsub)
	      val nexp2 = subst_exp (e2, subexp, newsub)
	  in  I.BinopExp(nexp1, bop, nexp2, pos)
	  end
	| I.Not(e,p) => 
	  let val nexp1 = subst_exp(e,subexp,newsub)
	  in I.Not(nexp1,p)
	  end
	| I.Result =>
	  let fun cutoff(I.Upd(l, I.Expvoid, e)) = 
		  (case e
		   of I.Expvoid => raise Fail "Return type of function is VOID"
		    | _ => e)
		| cutoff _ = raise Fail "error in RESULT"
	      val var = Id.fromString "hack_result"
	  in  case subexp
	       of I.Var(var, 0) => cutoff newsub
	        | _ => I.Result
	  end
	| I.Imply(e1, e2, p) => 
	  let val nexp1 = subst_exp(e1,subexp,newsub)
	      val nexp2 = subst_exp(e2,subexp,newsub)
	  in I.Imply(nexp1,nexp2,p)
	  end
	| I.Forall(id, tp, e1, pos) => 
	  (case subexp
	    of I.Var(id1, pos1) => if Id.equals (id, id1)
	                           then I.Forall(id, tp, e1, pos)
	                           else I.Forall(id, tp, subst_exp(e1, subexp, newsub), pos1)
	     | _ => I.Forall(id, tp, subst_exp(e1, subexp, newsub), pos))
	| I.Exists(id,tp,e1,p) => 
	  let val nexp1 = subst_exp(e1,subexp,newsub)
	  in I.Exists(id,tp,nexp1,p)
	  end
	| I.Pi(lvalsl,p) => I.Pi(lvalsl,p)
	| I.N(lvals,p) => I.N(lvals,p)
	| I.D(lvals,p) => I.D(lvals,p)
	| I.Prev(lval,p) => I.Prev(lval,p)
	| I.LList(e, pos) =>
	  let val e' = subst_exp(e, subexp, newsub)
	  in  I.LList(e', pos)
	  end   
	| I.Tree(e, pos) =>
	  let val e' = subst_exp(e, subexp, newsub)
	  in  I.Tree(e', pos)
	  end
	| I.Pred(id, exp, pos) => I.Pred(id, exp, pos)
	| I.Let(e1, e2, e3, pos) => I.Let(e1, e2, e3, pos)

  and subst_lval (lval, subexp, newsub) = 
      case lval
       of I.Var (id, pos) => vcgensimple(I.Var(id, pos), newsub)
	| I.Ptr (tp, lval1, pos) => 
          (raise Fail "no this case\n";
	   let val newtp = subst_lval(tp, subexp, newsub)
	   in  I.Ptr(newtp, lval1, pos)
	   end)
	| I.Inarray (lval1, e1, sz, p) => raise Fail "no this case\n"
	| I.Instruct (lval1, id1, p) => raise Fail "no this case\n"
        | I.Instruct2 (lval1, id1, id2, pos) => raise Fail "no this case\n"
	| I.Upd (l,e1,e2) =>
	  let val newl = subst_lval(l, subexp, newsub)
	      val newe1 = subst_exp(e1, subexp, newsub)
	      val newe2 = subst_exp(e2, subexp, newsub)
	  in  I.Upd(newl, newe1, newe2)
	  end
	| I.Sel (l, e) =>
	  let val newlval = subst_lval(l, subexp, newsub)
	      val newe = subst_exp(e, subexp, newsub)
	  in I.Sel(newlval, newe)
	  end
	| I.Sharp tp =>
	  (case subexp
	    of I.Sharp(tp') =>
	       if I.eqTipe (tp, tp')
	       then newsub
	       else I.Sharp tp
	     | _ => I.Sharp tp)	  

  fun represult(exp, fid) = 
      case exp
       of I.Expvoid => I.Expvoid
	| I.IntNum(i) => I.IntNum(i)
	| I.True => I.True
	| I.False => I.False
	| I.Null => I.Null
	| I.Lval(l) => I.Lval(l)
	| I.BinopExp(e1,bop,e2,p) => 
	  let val nexp1 = represult(e1, fid)
	      val nexp2 = represult(e2, fid)
	  in  I.BinopExp(nexp1,bop,nexp2,p)
	  end
	| I.Not(e,p) => 
	  let val nexp1 = represult(e,fid)
	  in I.Not(nexp1,p)
	  end
	| I.Result => I.Lval(I.Var(Id.fromString ("hack_res_"^(Id.toString fid)),0))
	| I.Imply(e1,e2,p) => 
	  let val nexp1 = represult(e1,fid)
	      val nexp2 = represult(e2,fid)
	  in I.Imply(nexp1,nexp2,p)
	  end
	| I.Forall(id,tp,e1,p) => 
	  let val nexp1 = represult(e1,fid)
	  in I.Forall(id,tp,nexp1,p)
	  end
	| I.Exists(id,tp,e1,p) => 
	  let val nexp1 = represult(e1,fid)
	  in I.Exists(id,tp,nexp1,p)
	  end
	| I.Pi(lvalsl,p) => I.Pi(lvalsl,p)
	| I.N(lvals,p) => I.N(lvals,p)
	| I.D(lvals,p) => I.D(lvals,p)
	| I.Prev(lval,p) => I.Prev(lval,p)
	| I.LList(exp, pos) => raise Fail ""
	| I.Tree(exp, pos) =>
	  let val e' = ()
	  in  I.Tree(exp, pos)
	  end
	| _ => raise Fail ""
  
  fun subst (exp, sub, newsub) = 
      let fun simplify(I.Lval(I.Upd(l,I.Expvoid,e))) = e
	    | simplify(onode) = onode
      in  case sub
           of I.Var(id, pos) => subst_exp(exp, sub, newsub)
	    | I.Ptr(tp, lval, pos) =>
	      let val tmpe = simplify(I.Lval(newsub))
	          val new_lval = I.selectL lval
	      in  subst_exp(exp, tp, I.Upd(tp, I.Lval(new_lval), tmpe))
	      end
	    | I.Inarray(lval, e1, size, pos) => 
	      let val new_lval = I.selectL lval
	          val new_e1 = I.selectE e1
	          val newsub1 = I.Upd(new_lval, new_e1, simplify(I.Lval(newsub)))	          
	      in  subst (exp, lval, newsub1)
	      end
	    | I.Instruct(lval, id, pos) => 
	      let val newfield = I.Lval(I.Var(id, pos))
	          val new_lval = I.selectL lval
		  val newsub1 = I.Upd(new_lval, newfield, simplify(I.Lval(newsub)))
	      in  subst(exp, lval, newsub1)
	      end
	    | _ => raise Fail "no this case\n"
      end
      
  fun collect stm =
      case stm
       of I.Skip => e_set
        | I.AsnExp(I.Var(id, pos1), exp, ty, pos2) => Set.add(e_set, Id.toString id)
        | I.AsnExp(_, e, ty, pos) => raise Fail "not implemented yet\n"
        | I.AsnAlloc(I.Var(id, pos1), mytype, bty, pos2) => Set.add(e_set, Id.toString id)
        | I.AsnAlloc(_, ty, bty, pos) => raise Fail "not impl yet\n"
        | I.AsnCall(I.Var(id1, pos1), id2, es, ty, pos2) => Set.add(e_set, Id.toString id1)
        | I.AsnCall(_, id, es, ty, pos) => raise Fail "not implemented yet\n"
        | I.Seq(s1, s2, pos) => Set.union(collect s1, collect s2)
        | I.If(e, s1, s2, pos) => Set.union(collect s1, collect s2)
        | I.While(inv, e, s, pos) => collect s
        | I.Return(e, pos) => e_set
        | I.Call(id, es, pos) => e_set
        | I.Free(e, pos) => e_set         
        | I.Prop(e, pos) => e_set
     
  fun vc_stm (stmt, q, postc) = 
      let fun gen(I.Skip) = I.Seq(I.Prop(q, 0), I.Skip, 0)
	    | gen(I.AsnExp(lval, exp, ty, pos)) = 
	      let val side_lval = side_lval lval
		  val side_exp = side_exp exp
		  val side_all = conj(side_lval, side_exp, pos)
		  val sel_exp = I.selectE exp
		  val pre_cond = subst (q, lval, I.Upd(lval, I.Expvoid, sel_exp))
		  val prop = conj(pre_cond, side_all, pos)
	      in  I.Seq(I.Prop(prop, pos), I.AsnExp(lval, exp, ty, pos), pos)
	      end
	    | gen(I.AsnAlloc(lval, tp, bty, pos)) =
	      let val side_lval = side_lval lval
	          val fresh_ptr = T.new_ptr()
	          val fresh_var = I.Lval(I.Var(Id.fromString fresh_ptr, 0))
	          val new_p = I.Lval(I.Sel(I.Sharp(I.Void), fresh_var))
	          val new_q = subst (q, lval, I.Upd(lval, I.Expvoid, fresh_var))
	          val all1 = I.Imply(new_p, new_q, pos)
	          val all = conj (all1, side_lval, pos)
	      in  I.Seq(I.Prop(all, pos), I.AsnAlloc(lval, tp, bty, pos), pos)
	      end
	    | gen(I.AsnCall(lval, fid, es, ty, pos)) = 
	      let val side_es = side_es(es, pos)
		  val side_lval = side_lval lval
		  val side_all = conj(side_es, side_lval, pos)
		  val sel_es = I.selectEs es
		  val alist = f_alist(fid, pos)
		  val (prec, postc) = f_pre_post fid
		  val ref_prec = ref(prec)
		  val ref_postc = ref(postc)		  
		  fun modcond([], [], condref) = ()
		    | modcond((a0)::al, (e0)::el, condref) = 
		      let val newp = I.Upd(a0, I.Expvoid, e0)
		      in  (condref:= subst_exp (!condref, a0, newp);
			  modcond(al, el, condref))
		      end
		    | modcond(_, _, _) = raise Fail "bug"
		  val _ = modcond(alist, sel_es, ref_prec)
		  val _ = modcond(alist, sel_es, ref_postc)
		  val prop1 = !ref_prec
		  val prop1' = !ref_postc
		  val new_fid = Id.fromString ("hack_res_"^(Id.toString fid))
		  val resnode = I.Lval(I.Var(new_fid, pos))
		  val prop2 = subst (q, lval, I.Upd(lval, I.Expvoid, resnode))
		  val prop31 = I.Imply(represult(prop1', fid), prop2, pos)
		  val prop3 = I.Forall(new_fid, I.Int, prop31, pos)
		  val prop' = conj(prop1, prop3, pos)
		  val prop = conj(prop', side_all, pos)
	      in  I.Seq(I.Prop(prop, pos), I.AsnCall(lval, fid, es, ty, pos), pos)
	      end
	    | gen(I.Seq(s1, s2, pos)) = 
	      let val ntree = vc_stm (s2, q, postc)
		  val tmp_node = I.Seq(s1, ntree, pos)
		  val (nq, _) = split ntree
		  val ntree1 = vc_stm (s1, nq, postc)
		  val (nq1, _) = split ntree1
	      in I.Seq(I.Prop(nq1, pos), tmp_node, pos)
	      end
	    | gen(I.If(cond', s1, s2, pos)) = 
	      let val side_e = side_exp cond'
		  val sel_e = I.selectE cond'
		  val ttree = vc_stm (s1, q, postc)
		  val ftree = vc_stm (s2, q, postc)
		  val tmp_node= I.If(cond', ttree, ftree, pos)
		  val (tq, _) = split ttree
		  val (fq, _) = split ftree
		  val prop' = conj(I.Imply(sel_e, tq, pos), I.Imply(I.Not(sel_e, pos), fq, pos), pos)
		  val prop = conj(prop', side_e, pos)
	      in I.Seq(I.Prop(prop, pos), tmp_node, pos)
	      end
	    | gen(I.While(inv, cond, s, pos)) =
	      let val side_cond = side_exp cond
	          val side_inv = side_exp inv
	          val side_all = conj(side_cond, side_inv, pos)
		  val sel_inv = I.selectE inv
		  val sel_cond = I.selectE cond
		  val ltree = vc_stm (s, sel_inv, postc)
		  val (s_prop, _) = split ltree
		  val tmpnode = I.While(inv, cond, ltree, pos)                
                  val vc_e = I.Imply(sel_inv, I.Imply(sel_cond, s_prop, pos), pos)
                  val vc_ne = I.Imply(sel_inv, I.Imply(I.Not(sel_cond, pos), q, pos), pos)
                  val _ = new_lvc vc_e vc_ne pos		
		  fun add_forall lvals exp =
		      let fun g ([]) = exp
		            | g (id::xs) = add_forall xs (I.Forall(id, I.Int, exp, pos)) 
		      in  g lvals
		      end
		  val prop1 = sel_inv
		  val prop = conj (prop1, side_all, pos)
	      in  I.Seq(I.Prop(prop, pos), tmpnode, pos)
	      end
	    | gen(I.Return(e, pos)) = 
	      let val side_e = side_exp e
		  val sel_e = I.selectE e
		  val tmplval = I.Var(Id.fromString"hack_result", 0)
		  val castexp = I.Upd(tmplval, I.Expvoid, sel_e)
		  val prop' = subst_exp (postc, tmplval, castexp)
		  val prop = conj (prop', side_e, pos)
	      in  I.Seq(I.Prop(prop, pos), I.Return(e, pos), pos)
	      end
	    | gen(I.Call(fid, es, pos)) = 
	      let val side_es = side_es (es, pos)
		  val sel_es = I.selectEs es
		  val alist = f_alist (fid, pos)
		  val (prec, postc) = f_pre_post fid
		  val tmpprec = ref(prec)
		  val tmppostc = ref(postc)
		  fun modcond([],[],condref) = ()
		    | modcond((a0)::al, (p0)::pl, condref) = 
		      let val newp = I.Upd(a0,I.Expvoid,p0)
		      in  (condref:= subst_exp (!condref, a0, newp);
			  modcond(al,pl,condref))
		      end
		    | modcond(_, _, _) = raise Fail "not implemented yet\n"
		  val _ = modcond(alist, sel_es, tmpprec)
		  val _ = modcond(alist, sel_es, tmppostc)
		  val prop1 = !tmpprec
		  val prop1' = !tmppostc
		  val prop21 = I.Imply(represult(prop1', fid), q, pos)
		  val prop2 = I.Forall(Id.fromString ("hack_res_"^(Id.toString fid)), I.Int, prop21, pos)
		  val prop' = conj (prop1, prop2, pos)
		  val prop = conj(prop', side_es, pos)
	      in  I.Seq(I.Prop(prop, pos), I.Call(fid, es, pos), pos)
	      end
	    | gen(I.Free(e, pos)) = 
	      let val side_e = side_exp e
	          val sel_e = I.selectE e
	      in I.Seq(I.Prop(side_e, pos), I.Free(e, pos), pos)
	      end
	    | gen(I.Prop(exp, pos)) = raise Fail "no this case..."
      in  gen stmt
      end 

  fun vc_fun (prec, stmts, postc, pos) = 
      let val newtree = vc_stm (stmts, postc, postc) 
	  val (prop, new_stm)= split newtree
      in  I.Imply(prec, prop, pos)
      end
  
  fun get_from_let (I.Let(e1, e2, e3, pos)) = e3
    | get_from_let e = e
    
  fun vc_top t = 
      case t
       of I.ExdecSkip => []
        | I.ExdecSeq(ex1, ex2, pos) => vc_top (ex1) @ vc_top (ex2)
        | I.ExdecStruct(id, flist, pos) => []
        | I.ExdecVar(ilist, pos) => []
        | I.ExdecFunc(id, rtp, alist, llist, stms, prec, postc, pos) => 
          let val _ = reset_lvc()
              val pre = get_from_let prec 
              val pot = get_from_let postc
	      val sel_pre = I.selectE pre
	      val sel_post = I.selectE pot
	      val top_vc = vc_fun(sel_pre, stms, sel_post, pos)
	      val lvc = get_lvc()
          in  (id, top_vc)::lvc
          end

  fun vcgenstep1 exdecnode = 
      let val libfunc = (Id.fromString "printp", [(Id.fromString "p", I.Pointer(I.Void))], I.True, I.True)::
			(Id.fromString "print",  [(Id.fromString "i",I.Int)],              I.True, I.True)::
			(Id.fromString "printb", [(Id.fromString "i",I.Bool)],             I.True, I.True)::
			(Id.fromString "alloc",  [(Id.fromString "i",I.Int)],              I.True, I.True)::
			(Id.fromString "free",   [(Id.fromString "ppp",I.Pointer(I.Void))],I.True, I.True)::[]
	  fun step1(I.ExdecSkip) = []
	    | step1(I.ExdecSeq(ex1, ex2, pos)) = step1(ex1)@step1(ex2)
	    | step1(I.ExdecStruct(id, flist, pos)) = []
	    | step1(I.ExdecVar(ilist, pos)) = []
	    | step1(I.ExdecFunc(id, rtp, alist, llist, stms, prec, postc, pos)) = 
	      [(id, alist, I.selectE (get_from_let prec), I.selectE (get_from_let postc))]
      in  funcs := step1(exdecnode) @ libfunc
      end
  
  fun top ir = 
      let val _ = vcgenstep1 ir
	  val proplist = vc_top ir
      in  proplist
      end
end



